Inference at * 2 
Iof proof for Lemma nth tl is fseg:



1. T : Type
2. L1 : T List
3. L2 : T List
4. n : {0..(||L2||+1)}
5. L1 = nth_tl(n;L2)
  L:T List. (L2 = (L @ L1)) 

latex

 by ((InstConcl [firstn(n;L2)]) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1:   L2 = (firstn(n;L2) @ L1)
C.

Definitions	firstn(n;as), x:A. B(x), x:A  B(x), , nth_tl(n;as), Type, as @ bs, x:A. B(x), x:AB(x), t  T, s = t, type List, {i..j}
Lemmas	firstn wf, append wf